\begin{tabbing}
$\vdash$  \=$\forall$$A$:Type, $n$, $m$:$\mathbb{N}$, $f$:($A$$\rightarrow$($A$ + Top)), $x$:$A$.\+
\\[0ex]($\uparrow$can{-}apply($f$\^{}$n$+$m$;$x$))
\\[0ex]$\Rightarrow$ \=\{($\uparrow$can{-}apply($f$\^{}$m$;$x$))\+
\\[0ex]\& ($\uparrow$can{-}apply($f$\^{}$n$;do{-}apply($f$\^{}$m$;$x$)))
\\[0ex]\& do{-}apply($f$\^{}$n$+$m$;$x$) = do{-}apply($f$\^{}$n$;do{-}apply($f$\^{}$m$;$x$))\}
\-\-
\end{tabbing}